Section: New Results

Automatic Array Content Analysis by Segmentation

Participants : Patrick Cousot, Radhia Cousot, Francesco Logozzo [Microsoft Research (Redmond, USA)] .

In [18] , we introduce FunArray , a parametric segmentation abstract domain functor for the fully automatic and scalable analysis of array content properties. The functor enables a natural, painless and efficient lifting of existing abstract domains for scalar variables to the analysis of uniform compound data-structures such as arrays and collections (as well as matrices when instantiating the functor on itself). The analysis automatically and semantically divides arrays into consecutive non-overlapping possibly empty segments. Segments are delimited by sets of bound symbolic expressions and abstracted uniformly. All bound expressions appearing in a set are equal in the concrete. The FunArray can be naturally combined via reduced product with any existing analysis for scalar variables. The bound expressions, the segment abstractions and the reduction operator are the three parameters of the analysis. Once the functor has been instantiated with fixed parameters, the analysis is fully automatic.

We first prototyped FunArray in Arrayal to adjust and experiment with the abstractions and the algorithms to obtain the appropriate precision/ratio cost. Then it was implemented into CCCheck (formerly Clousot ), an abstract interpretation-based static contract checker for .NET by Francesco Logozzo. The precision and the performance of the analysis has been empirically validated by running it on the main libraries of .NET and on its own code. It was able to infer thousands of invariants and to verify the implementation with a modest overhead (circa 1%). To the best of our knowledge this is the first analysis of this kind applied to such a large code base, and proven to scale.